package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class ToyS2 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("ToyS2");
		 
         // Variables
		 TypedData y = new TypedData("y", Constants.TYPE_INTEGER);
		 tiosts.addVariable(y);
         
         // There are no parameters       
         
         Action init2 = new Action("Init2", Constants.ACTION_INTERNAL);
         tiosts.addAction(init2);
         Action aInput = new Action("a", Constants.ACTION_INPUT);
         tiosts.addAction(aInput);
         tiosts.addActionParameter(y);
         
         Action aOutput = new Action("a", Constants.ACTION_OUTPUT);
         tiosts.addAction(aOutput);     
         
         Action c = new Action("c", Constants.ACTION_INPUT);
         tiosts.addAction(c);   
         
         Location start2 = new Location("Start2");
         tiosts.addLocation(start2);
         Location s3 = new Location("S3");
         tiosts.addLocation(s3);
         Location s4 = new Location("S4");
         tiosts.addLocation(s4);        
         Location s5 = new Location("S5");
         tiosts.addLocation(s5);
         Location lc2 = new Location("lc2");
         tiosts.addLocation(lc2);
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start2);
         
         // Transitions
         tiosts.createTransition("Start2", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init2, null, null, "S3");
         tiosts.createTransition("S3", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, "y := 0", null, "S4");
         tiosts.createTransition("S4", "y > 5", Constants.GUARD_TRUE, aInput, null, null, "S5");
         tiosts.createTransition("S5", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aOutput, null, null, "S5");
         tiosts.createTransition("S3", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc2");
         tiosts.createTransition("S4", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, null, null, "lc2");
         tiosts.createTransition("S4", "y <= 5", Constants.GUARD_TRUE, aInput, null, null, "lc2");
         tiosts.createTransition("S5", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc2");
         tiosts.createTransition("S5", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, null, null, "lc2");
         
         return tiosts;		 
	 }

}
